#|===== Module: io-utilities =========================================

 Defining
   string-list->file        write file
   file->string             read file
   rat->str                 convert rational number to string
   str->rat                 convert string to rational number
   loc                      report LoC for specified file

 (string-list->file file-path list-of-strings state)
    Produces effect of writing strings to specified file, in sequence
    with newline-characters added at the end of each string
    Note: Directory separator in file-path string must be "/", not "\"
    Note: "Example functions" section shows how to use this function
          See: (wfoo state), (rwfoobar state)
    Note: Returns multiple value containing error status and state

 (file->string file-path state)
    delivers (mv string error state) where string contains all characters
    in the file
    Note: Directory separator in file-path string must be "/", not "\"
    Note: "Example functions" section shows how to use this function
          See: (rfoo state), (rwfoobar state)
    Note: Returns multiple value containing characters from file as
          string, error status, and state
    Warning! Reading very big files might exhaust virtual memory

 (rat->str r d)
     delivers string containing decimal representation of a rational
     number, r, with d decimal places digits following the decimal.

 (str->rat str)
    delivers rational number represented by str, a string of decimal 
    digits, possibly containing a decimal point, and possibly with a
    leading +/- sign

 (loc file-path state)
    Reports number of lines of code in file specified by file-path 
    (a string). Also reports state, which is annoying
====================================================================|#

#|===== Usage Note ===================================================
 Where to put this file:
 
   * SE-Projects (this name does not matter)
   |- SE    (must use this name)
   |  |- io-utilities.lisp   
   |  |- list-utilities.lisp
   |
   |- iEx0  (name does not matter)
   |  |- iEx0.ezpsp
   |  |- iEx0.lisp
   |
   |- iEx1  (name does not matter)
   |  |- iEx1.ezpsp
   |  |- iEx1.lisp
   | 
   | etc...

 To certify this module, open it in DrACuLa and press Save/Certify

 Warning! This book imports list-utilities
          Make sure a certified list-utilities book is in
          the same folder with this one

 To make definitions in this module available in a module residing
 in iEx0, iEx1, ..., put the following commands in that module:
 Note: The definitions in list-utilities also become available
       in the module that imports this one
   (include-book "../SE/io-utilities")
   (set-state-ok t)
====================================================================|#

;===== Environment setup =============================================
 (in-package "ACL2")
 (set-compile-fns t)
 (include-book "list-utilities")
 (set-state-ok t)
;=====================================================================

#|===== Function: (dgt->chr dgt) =====================================

  Converts integer in 0-9 range to digit-character

  Pre : (member-equal dgt '(0 1 2 3 4 5 6 7 8 9))
  Post: (member-equal (dgt->chr dgt) 
                      '(#\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9)
  Note: defaults to #\0 if dgt is not a one-digit, nonnegative integer
====================================================================|#
(defun dgt->chr (dgt)
   (cond ((equal dgt 0) #\0)
         ((equal dgt 1) #\1)
         ((equal dgt 2) #\2)
         ((equal dgt 3) #\3)
         ((equal dgt 4) #\4)
         ((equal dgt 5) #\5)
         ((equal dgt 6) #\6)
         ((equal dgt 7) #\7)
         ((equal dgt 8) #\8)
         ((equal dgt 9) #\9)
         (t             #\0)))

#|====== Function: (dgts->chrs dgts) =================================

  Converts every digit in a list to the corresponding character

  Pre : (and (integer-listp dgts)
             (implies (and (integerp d) (member d dgts))
                      (member d '(0 1 2 3 4 5 6 7 8 9)))
  Post: (implies (and (characterp c) (member c (dgts->char dgts)))
                 (member c (#\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9)))
====================================================================|#
(defun dgts->chrs (dgts)
   (if (not (consp dgts))
       nil
       (cons (dgt->chr (car dgts))
             (dgts->chrs (cdr dgts)))))

#|===== Function: (chr->dgt dgt-chr) =================================

  Converts a digit-character to the corresponding one-digit integer

  Pre : (member-equal dgt-chr 
                      '(#\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9))
  Post: (member (char->dgt dgt-chr) '(0 1 2 3 4 5 6 7 8 9))
  Note: defaults to 0 if dgt-chr is not a digit character
====================================================================|#
(defun chr->dgt (chr)
   (cond ((equal chr #\0) 0)
         ((equal chr #\1) 1)
         ((equal chr #\2) 2)
         ((equal chr #\3) 3)
         ((equal chr #\4) 4)
         ((equal chr #\5) 5)
         ((equal chr #\6) 6)
         ((equal chr #\7) 7)
         ((equal chr #\8) 8)
         ((equal chr #\9) 9)
         (t               0)))

#|====== Function: (chrs->dgts chrs) =================================

  Converts every digit in a list to the corresponding character

  Pre : (and (character-listp chrs)
             (implies (and (characterp c) (member c chrs))
                      (member c '(#\0 #\1 #\2 #\3 #\4 
		                 #\5 #\6 #\7 #\8 #\9))
  Post: (implies (and (integerp d) (member d (chrs->dgts chrs)))
                 (member d '(0 1 2 3 4 5 6 7 8 9)))              
====================================================================|#
(defun chrs->dgts (chrs)
   (if (not (consp chrs))
       nil
       (cons (chr->dgt (car chrs))
             (chrs->dgts (cdr chrs)))))

#|===== Function: (horner s x coefficients) ==========================

  Computes s*(x^n) + polynomial in x with given coefficients
    where n = (length coefficients)
  Note: Coefficient list ordering is high-order to low-order
        That is, (nth k coefficients) is coefficient of x^(n - k - 1)
        where n = (length coefficients) - 1, k = 0, 1, ... n-1

  Pre : (and (numberp s) (numberp x) (number-listp coefficients))
  Post: (integerp (horner s x coefficients))
====================================================================|#
(defun horner (accumulator x coefficients )
  (if (not (consp coefficients))
       accumulator
       (horner (+ (car coefficients) (* x  accumulator))
               x
               (cdr coefficients))))

#|===== Function: (dgts->int dgts) ===================================

  Delivers integer whose decimal digits comprise dgts 
  (high-order to low-order)

  Pre : (implies (member-equal d dgts)
                 (member-equal d '(0 1 2 3 4 5 6 7 8 9)))
  Post: (and (integerp (dgts->int dgts))
             (>= (dgts->int dgts) 0))
====================================================================|#
(defun dgts->int (dgts)
  (horner 0 10 dgts))

#|===== Function: (int->append-dgts n dgts) ==========================

  Append dgts to digits of decimal representation of n

  Pre:  (and (integerp n) (>= n 0)
             (implies (member-equal d dgts)
                      (member-equal d '(0 1 2 3 4 5 6 7 8 9))))
  Post: (equal (dgts->int (int->append-dgts n nil))
               n)
====================================================================|#
(defun int->append-dgts (n dgts)
   (if (or (not (integerp n))
           (not (> n 0)))
       dgts
       (int->append-dgts (floor n 10) (cons (mod n 10) dgts))))

#|===== Function: (int->dgts n) ======================================

  Deliver digits of decimal representation of n

  Pre:  (and (integerp n) (>= n 0))
  Post: (equal (dgts->int (int->dgts n))
               n)
====================================================================|#
(defun int->dgts (n)
  (int->append-dgts n nil))

#|===== Function: (str->int str) =====================================

  Returns integer represented by string

  Pre:  (implies (member-equal chr (str->chrs str))
                 (member-equal chr '(#\0 #\1 #\2 ... #\9)))
  Post: (str->int str) is the integer specifed, in decimal notation, 
        in str
====================================================================|#
(defun str->int (str)
   (dgts->int (chrs->dgts (str->chrs str))))

#|===== Function: (int->str n) =======================================

  Returns string containing decimal representation of n

  Pre:  (and (integerp n)
             (>= n 0))
  Post: (equal (str->int (int->str n))
               n)
====================================================================|#
(defun int->str (n)
   (chrs->str (dgts->chrs (int->dgts n))))

#|===== Function: (str->rat str) =====================================

  Returns number whose decimal representation is str

  Pre:  (and (implies (member chr (str->chrs str))
                      (or (member chr '(#\0 #\1 #\2 ... #\9))
                          (equal chr #\+)
                          (equal chr #\-)
                          (equal chr #\.))
             (not (member #\+ (drop-past #\+ (str->chrs str))))
             (not (member #\- (drop-past #\+ (str->chrs str))))
             (not (member #\- (drop-past #\- (str->chrs str))))
             (not (member #\+ (drop-past #\- (str->chrs str)))))
  Post: (and (rationalp (str->rat str))
             (= (str->rat str)
                (str->rat (rat->str (str->rat str) (length str)))))
  Note: (equal (str->rat nil) 0)
  Note: Defaults to zero if str does not meet expectations
====================================================================|#
(defun str->rat (str)
  (if (or (not (stringp str))
          (string-equal str ""))
      0
      (let* ((chrs (str->chrs str))
             (maybe-sign (car chrs))
             (sans-sign (if (member maybe-sign '(#\+ #\-))
                            (cdr chrs)
                            chrs))
             (parts (break-at #\. sans-sign))
             (int-part (car parts))
             (frc-part (cdr (cadr parts)))
             (int-dgts (chrs->dgts int-part))
             (frc-dgts (chrs->dgts frc-part))
             (r-magnitude  (+ (dgts->int int-dgts)
                              (/ (dgts->int frc-dgts)
                                 (expt 10 (length frc-dgts))))))
        (if (char-equal maybe-sign #\-)
            (- r-magnitude)
            r-magnitude))))

#|===== Function: (rat->str r d) =====================================

  Returns string containing decimal representation of r, to d decimal 
   places

  Pre:  (and (rationalp r)
             (integerp d)
             (>= d 0))
  Post: (<= (abs(- (str->rat (rat->str r d))
                    r))
            (/ 5 (expt 10 (+ d 1))))
  Note: Defaults to "0" if parameters fail to meet expectations
====================================================================|#
(defun rat->str (r d)
  (if (or (not (rationalp r))
          (= r 0)
          (not (integerp d))
          (< d 0))
      "0"
  (let* ((r-shifted (round (* (abs r) (expt 10 d)) 1))
         (r-chrs (dgts->chrs (int->dgts r-shifted)))
         (n (length r-chrs))
         (num-dgts-before-decimal-pt (max 0 (- n d)))
         (minus-sign-if-needed (if (< r 0) '(#\-) nil)) 
         (parts (break-at-nth num-dgts-before-decimal-pt r-chrs))
         (int-part (car parts))
         (decimal-pt-if-needed (if (> d 0) '(#\.) nil))
         (frc-part (cadr parts)))
    (chrs->str (append minus-sign-if-needed
                       int-part
                       decimal-pt-if-needed
                       (pad-left d #\0 frc-part))))))

#|===== (read-n-chars n li channel state) ============================

  Inserts up to n characters from channel into li, leaving the new 
  characters at the beginning of li in the reverse of the order 
  in they were received in

  Pre : (and (integerp n)
             (>= n 0)
             (character-listp li)
             (character-input-channelp channel))
  Post: Up to n characters have been received from channel
        Returns multiple value containing list of chars, channel, 
	and state
====================================================================|#
(defun read-n-chars (n li channel state)
   (if (or (not (integerp n)) (<= n 0))
       (mv li channel state)
       (mv-let (chr state) (read-char$ channel state)
          (if (null chr)
              (mv li channel state)
              (read-n-chars (- n 1) (cons chr li) channel state)))))

#|===== (write-all-strings strli channel state) ======================

  Writes characters from each string in strli to channel
  (inserting a newline after the characters comprising each element 
  of strli)

  Pre : (and (string-listp strli)
             (character-input-channelp channel))
  Post: channel has received chars from strings in strli, plus 
        newlines. Returns multiple value containing channel and new 
	state
====================================================================|#
(defun write-all-strings (strli channel state)
   (if (endp strli)
       (mv channel state)
       (let ((state (princ$ (string-append (car strli)
                                        (coerce '(#\newline) 'STRING))
                            channel 
                            state)))
          (write-all-strings (cdr strli) channel state))))

#|===== (file->string file-path state) ===============================

  Makes character sequence comprising file accessible as string

  Pre : (character-listp file-path)
  Post: Characters in file become accessible as string portion
          of returned multiple value
        Returns multiple value:
          (1) string comprising first million characters from file
          (2) status (nil indicates success)
          (3) state
  Warning! System may run out of virtual memory when reading big files
  Warning! This function will not read files exceeding about 4GB
====================================================================|#
(defun file->string (fname state)
   (mv-let (chli error state)
           (mv-let (channel state) 
		   (open-input-channel fname :character state)
              (if (null channel)
                  (mv nil
                      (string-append "Error opening file for input: "
                                     fname)
                      state)
                  (mv-let (chlist chnl state)
                          (read-n-chars 4000000000 '() channel state)
                     (let ((state (close-input-channel chnl state)))
                       (mv chlist nil state)))))
      (mv (reverse (chrs->str chli)) error state)))

#|===== (string-list->file list-of-strings file-path state) ==========

  Writes strings to specified file, in sequence, and with
  newline characters added at the end of each string

  Pre:  (and (string-listp list-of-strings)
             (character-listp file-path))
  Post: Designated file contains characters from list-of-strings
          with newline characters inserted
        Returns multiple value:
          (1) status (nil indicates success)
          (2) state
====================================================================|#
(defun string-list->file (fname strli state)
  (mv-let (channel state)
          (open-output-channel fname :character state)
     (if (null channel)
         (mv (string-append "Error opening file for output: " fname)
             state)
         (mv-let (channel state)
                 (write-all-strings strli channel state)
            (let ((state (close-output-channel channel state)))
              (mv nil state))))))

#|===== (loc file-path state) ========================================

  Reports number of lines of code in file specified by file-path 
  (a string).  Also reports state, which is annoying

 Note: Lines consisting entirely of commentary or whitespace
       are not counted as lines of code
 Warning! Unix-style path names required ("dir/nam", not "dir\nam")
 WARNING! The input file must use Unix-style line-terminators.
          If you created the file using Notepad or Wordpad,
          you must convert it to Unix style, which you can do like 
	     this: dos2unix "some-program.lisp"
          Of course, you'll need to convert the file back to Windows 
	  style (unix2dos) when you want to edit it
 Sample usage:
 First:
   Copy file to be LoC-counted to a convenient place and convert to
   Unix-style line terminators, eg by using the following DOS commands
   copy "c:\ACL2-3.2\Sources\Books\SE\io-utilities.lisp" c:\
   dos2unix c:\io-utilities.lisp
 Then, in an ACL2 session:
   (include-book "io-utilities")
   (set-state-ok t)
   :comp read-n-chars ; Warning! This cmd is for sessions only, 
                        not books
   (loc "c:/io-utilities.lisp" state)
 Response in ACL2 session:
   (177 <state>)
====================================================================|#

(defun num-noncomments (lines count)
   (if (not (consp lines))
       count
       (let* ((whitespace '(#\Space #\Newline #\Tab))
              (leading-white-stripped (drop-set whitespace 
			                        (car lines))))
         (if (and (consp leading-white-stripped)
                  (not (char-equal #\; (car leading-white-stripped))))
             (num-noncomments (cdr lines) (+ count 1))
             (num-noncomments (cdr lines) count)))))
(defun loc-from-file-as-string (str)
  (num-noncomments (packets #\Newline (str->chrs str)) 0))
(defun loc (file-path state)
  (mv-let (str error state) (file->string file-path state)
     (if error
         (mv error state)
         (mv (loc-from-file-as-string str) state))))

#|===== Example functions using file i/o =============================

  Warning!
    The variable "state"
      (1) cannot have any other name
      (2) can be used only in certain contexts

  Note: You must issue the command
           (set-state-ok t)
        before invoking any function that refers to the variable state

  Note: Directory separator in file-path string is "/", not "\"

 (wfoo state)   ; This formula writes the file "C:/foo.wpd"
                  Well...actually...it's "C:\foo.wpd"
                  but ACL2 uses Unix conventions in path names
====================================================================|#

(defun wfoo (state)
  (mv-let (error state)
          (string-list->file "C:/foo.wpd"
                             (list "this is the first line"
                                   "this is the second line")
                             state)
     (if error
         (mv error state)
         (mv "Write C:/foo.wpd succeeded" state))))

; (rfoo state)   ; This formula reads the file "C:/foo.wpd"
;                  Well...actually...it's "C:\foo.wpd" 
;                  but ACL2 uses Unix conventions in path names

(defun formula-for-rfoo-result (str)
  (string-append "input file as string follows: " str))

(defun rfoo (state)
  (mv-let (str error state) (file->string "C:/foo.wpd" state)
     (if error
         (mv error state)
         (mv (formula-for-rfoo-result str) state))))

; (rwfoobar state)  ; This formula reads the file "C:/foo.wpd"
;                     then writes the file "C:/bar.wpd"
;                     (Well, it's "C:\foo.wpd" and "C:\bar.wpd"
;                     but ACL2 uses Unix conventions in path names)

(defun rwfoobar (state)
  (mv-let (input-as-string error-open state) 
	  (file->string "C:/foo.wpd" state)
     (if error-open
         (mv error-open state)
         (mv-let (error-close state)
                 (string-list->file "C:/bar.wpd"
                                    (list "c:/foo.wpd follows:"
                                          input-as-string)
                                    state)
            (if error-close
                (mv error-close state)
                (mv "Success: read c:/foo.wpd, wrote c:/bar.wpd" 
                     state))))))

; (map-chrs->str list-list-chrs); This formula applies chrs->str to
;                               ;   each element in a list in which 
;                               ;   each
;                               ;   element is a list of characters
;                               ; Thus, a list of lists of characters
;                               ;   becomes a list of strings

(defun map-chrs->str (list-list-chrs)
  (if (consp list-list-chrs)
      (cons (chrs->str (car list-list-chrs))
            (map-chrs->str (cdr list-list-chrs)))
      nil))

; (your-computation str) ; This formula converts a string to a list 
                         ;   strings each of which is a substring of 
			 ;   str filling in the gap between two 
			 ;   newline-characters
                         ; In a real program, this function would do a
			 ;   more elaborate computation, to carry out
			 ;   whatever transformation you intended your
			 ;   program to do, and then it would 
			 ;   represent the results of th comptutation
			 ;   as a list of strings

(defun your-computation (str)
  (map-chrs->str (packets #\Newline (str->chrs str))))
  
; (ipo f-in f-out state) ; This formula uses the function file->string
                         ;   reads the file f-in, producing a string 
			 ;   containing all the characters in the file
                         ; Then it invokes the function 
                         ;   "your-computation" to transform the 
			 ;   string to a list of strings
                         ; Finally, it writes the list of strings
                         ;   delivered by your-computation to a file 
                         ;   named f-out, one string per line
                         ; USING THIS INPUT/PROCESS/OUTPUT TEMPLATE
                         ;   Copy the defun for ipo,
                         ;   change its name to something appropriate,
                         ;   define a new function to do the
                         ;   computation you are working on (note: 
                         ;   your the input to your function will be a
                         ;   of all the characters from your input 
                         ;   file, string consisting and the output 
                         ;   must be  a list of strings, one string 
                         ;   for each line you want in your output 
                         ;   file), and, finally, replace the 
                         ;   invocation of "your-computation" by an 
			 ;   invoction of the function you defined
                         ; Warning! The input file f-in must be a 
                         ;   text-file with Unix-style line separators
                         ;   (You can convert DOS-style files to 
                         ;   Unix-style with the dos2unix program.)
                         ; Warning! The strings f-in and f-out must be
                         ;   Unix-style file-path specs, with forward 
                         ;   slashes not Windows-style back slashes
                         ;   For example, "C:/yourfolder/yourfile.wpd"
                         ;            not "C:\yourfolder\yourfile.wpd"
                         ; Warning! The third parameter of ipo cannot 
                         ;   be any symbol other than the symbol whose
                         ;    name is "state"
                         ; Warning! Before invoking this function from
                         ;   an ACL2 session, you must issue these 
			 ;   commands:
                         ;   (set-state-ok t)
                         ;   :comp read-n-chars
                         ;   :comp write-all-strings

(defun ipo (f-in f-out state)
  (mv-let (input-as-string error-open state) (file->string f-in state)
     (if error-open
         (mv error-open state)
         (mv-let (error-close state)
                 (string-list->file f-out
                                    (your-computation input-as-string)
                                    state)
            (if error-close
                (mv error-close state)
                (mv (string-append "Read "
                     (string-append f-in
                      (string-append ", compute, then write " f-out)))
                    state))))))
#|===== end of example functions ===================================|#
